es:ES, i:Id, k:Knd, L:(IdLnk List). @i:k sends only on links in L   

latex

Definitions	ES, t  T, Id, Knd, IdLnk, type List, P  Q, x:A. B(x), lnk(e), (x  l), sender(e), kind(e), s = t, , x:AB(x), loc(e), isrcv(e), b, Type, E, @i:k sends only on links in L
Lemmas	es-E wf, assert wf, es-isrcv wf, es-loc wf, es-kind wf, es-sender wf, l member wf, es-lnk wf, IdLnk wf, Knd wf, Id wf, event system wf